Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    fst(0,Z)  → nil
2:    fst(s,cons(Y))  → cons(Y)
3:    from(X)  → cons(X)
4:    add(0,X)  → X
5:    add(s,Y)  → s
6:    len(nil)  → 0
7:    len(cons(X))  → s
There are no dependency pairs. Hence the TRS is trivially terminating.
Tyrolean Termination Tool  (0.00 seconds)   ---  May 4, 2006